
%\documentclass[orivec]{llncs}
\documentclass[preprint]{elsarticle}
%\documentclass[10pt]{article} 
%
%\usepackage{makeidx}  % allows for indexgeneration

\usepackage{packages}





\newcommand{\mma}{Minsky machine\xspace}
\newcommand{\hide}[1]{}
\newcommand{\hof}{\ensuremath{\textsc{Ho}^{-\mathsf{f}}}\xspace}
\newcommand{\ahopi}{\hof}
\newcommand{\hopf}{\ensuremath{\textsc{HoP}^{-\mathsf{f}}}\xspace}
\newcommand{\hocore}{\ensuremath{\textsc{Hocore}}\xspace}

% Notation for definitions
\newcommand{\depth}[1]{\ensuremath{\mathsf{depth}(#1)}}
\newcommand{\maxDistance}[1]{\ensuremath{\mathsf{maxDistance}(#1)}}
\newcommand{\maxDist}[2]{\ensuremath{\mathsf{maxDist}_{#1}(#2)}}
\newcommand{\maxDepCom}[1]{\ensuremath{\mathsf{maxDepCom}(#1)}}
\newcommand{\deriv}[1]{\ensuremath{\mathsf{Deriv}(#1)}}

\pagestyle{plain}


\newcommand{\Ho}[2]{\overline{#1} \langle #2 \rangle}

\newcommand{\shortv}[1]{}%{#1}
\newcommand{\longv}[1]{#1}

% Height
%\addtolength{\voffset}{-0.45cm} 
%\addtolength{\textheight}{0.9cm} 
% Width
%\addtolength{\hoffset}{-0.45cm}
%\addtolength{\textwidth}{0.9cm} 

%\usepackage{hyperref}
%

\renewcommand{\vspace}[1]{}
%\renewcommand{\small}{}
%

%
%\mainmatter              % start of the contributions
%
%\title{On the Decidability of a Thread-Based Higher-Order Process Calculus}

\title{On the Expressiveness of Forwarding in Higher-Order Communication  \tnoteref{t1}}
\tnotetext[t1]{Supported 
by the French project ANR-2010-SEGI-013  - \textsc{Aeolus}, 
by the EU integrated project HATS, 
the Fondation de Coop\'eration Scientifique Digiteo Triangle de la Physique, 
by PEst-OE/EEI/UI0527/2011
Centro de Inform\'{a}tica e Tecnologias da Informa\c{c}\~{a}o (CITI/FCT/UNL) - 2011-2012, 
and by 
FCT / MCTES 
- Carnegie Mellon Portugal Program, grant NGN-44-2009-12
- \textsc{Interfaces}.}



\author[gre]{Cinzia Di Giusto}
\ead{cinzia-digiusto@inrialpes.fr} 
\address[gre]{INRIA Rh\^{o}ne Alpes, France}

\author[lis]{Jorge A. P\'erez}
\ead{japerezp@gmail.com} 
\address[lis]{CITI, Department of Computer Science, FCT New University of Lisbon, Portugal}

\author[bol]{Gianluigi Zavattaro}
\ead{zavattar@cs.unibo.it}
\address[bol]{Laboratory Focus (University of Bologna/INRIA), Italy}


%%\title{On the Expressiveness of Forwarding in Higher-Order Communication \longv{(\today)}\thanks{%Research partially supported by European Projects FET-GC II IST-2005-16004 \textsc{Sensoria} and 
%%Research partially funded by EU Integrated Projects
%%HATS (contract number 231620) and 
%%SENSORIA (contract number 016004).
%% }} 
%%%


\begin{document}


\begin{abstract} In higher-order process calculi the values exchanged in communications may
contain processes. 
There are only two capabilities for received processes: execution and forwarding.
Here we propose a limited form of forwarding:  output actions can only communicate the parallel composition of statically known closed processes and processes received through previously executed input actions. 
We study the expressiveness of a higher-order process calculus featuring this style of communication. 
Our main result shows that in this calculus termination is decidable while convergence is undecidable. 
%While the latter result is proved by an unfaithful encoding of Minsky machines, 
%the proof of the former result appeals to the theory of Well-Structured Transition Systems, in what appears to be the first time.
Then, as a way of recovering the expressiveness loss due to limited forwarding, we extend the calculus
with a form of process suspension called \emph{passivation}. 
Somewhat surprisingly, in the calculus extended with passivation both termination and convergence are undecidable.
\end{abstract}

\begin{keyword}
Process Calculi \sep Expressiveness and Decidability \sep Higher-Order Processes \sep Verification
\end{keyword}

\maketitle              % typeset the title of the contribution

% 
 \section{Introduction}
\input{chap-intro}

 \section{The Calculus}\label{s:lang}
 \input{lang}

 \section{Undecidability of Convergence in \hof}\label{s:turing}
 \input{minsky}

 \section{Decidability of Termination in \hof}\label{s:wsts}
 \input{finkel}
 \input{newlts}
 \input{termination}

 \section{On the Interplay of Fowarding and Passivation}\label{s:passiv}
\input{passivation}

%\input{altpassivation}
%\input{hierarchy}
%
%\input{ccs}
%
%\section{CCS rec + passivation}
%\input{ccsrec}

\section{Concluding Remarks}\label{s:conc}
\input{concl}



\bibliographystyle{model1b-num-names}
\bibliography{referen,DSbib}


\end{document}